#ifndef __PDTGRAPHCLONE_H_
#define __PDTGRAPHCLONE_H_

#include "PDTLinearTraverse.h"
#include <map>
#include <queue>

using namespace std;

class PDTCodeGraph;
class PDTNode;
class PDTVar;
class PDTPiAssign;

/* Extern functions */
extern bool isUsedBefore(PDTVar & d, bool & remove); 

class PDTGraphCloneTraversal : public PDTLinearTraversalIfc  {
public:
    PDTCodeGraph & rcg;
    PDTNode * topNode;
    PDTNode ** clones;
    map < unsigned int, PDTNode * > quantifierStatement;
    PDTPreCondition * pendingPre; // the current pre condition pending to resolve
    bool isFirstPre; // is first pre condition
    unsigned int preCount; // count of unresolved pre conditions

    unsigned int size;

    PDTGraphCloneTraversal(PDTCodeGraph & aOcg, PDTCodeGraph & aRcg, PDTNode * aTopNode = NULL);
    virtual ~PDTGraphCloneTraversal();

    PDTNode * getChildClone(PDTNode & d, unsigned int childNum) const;
    PDTNode * getClone(PDTNode & d) const;
    PDTNode * getClone(PDTNode * d) const;
    bool setClone(PDTNode & d, PDTNode * clone);
    bool setVarClone(PDTVar & d, PDTVar * clone);
    bool isTopNode(PDTNode * node) const;

    // has quantifier statement
    int hasQuantifier(PDTNode * stmt);

    // handle the quantifiers
    PDTNode * quantifierHandler(PDTNode * node, int childId);

    // fix variables initially
    Traversal::RetType fixVariables();

    // PDTAdd 
    virtual Traversal::RetType post(PDTAdd &);

    // PDTAnd 
    virtual Traversal::RetType post(PDTAnd &);


    // PDTAssert 
    virtual Traversal::RetType post(PDTAssert &);


    // PDTAssign 
    virtual Traversal::RetType post(PDTAssign &);


    // PDTBehavior 
    virtual Traversal::RetType post(PDTBehavior &);


    // PDTBehaviors 
    virtual Traversal::RetType post(PDTBehaviors &);
    //virtual Traversal::RetType pre(PDTBehaviors &);


    // PDTBoolConst 
    virtual Traversal::RetType post(PDTBoolConst &);


    // PDTBoolVar 
    virtual Traversal::RetType post(PDTBoolVar &);


    // PDTConstSequence 
    virtual Traversal::RetType post(PDTConstSequence &);


    // PDTDiv 
    virtual Traversal::RetType post(PDTDiv &);


    // PDTEqualBool 
    virtual Traversal::RetType post(PDTEqualBool &);


    // PDTEqualNum 
    virtual Traversal::RetType post(PDTEqualNum &);


    // PDTExist 
    virtual Traversal::RetType post(PDTExist &);


    // PDTForall 
    virtual Traversal::RetType post(PDTForall &);


    // PDTFunctionCall 
    virtual Traversal::RetType post(PDTFunctionCall &);


    // PDTFunctionDec 
    virtual Traversal::RetType post(PDTFunctionDec &);


    // PDTGreaterThan 
    virtual Traversal::RetType post(PDTGreaterThan &);


    // PDTGreaterThanEqual 
    virtual Traversal::RetType post(PDTGreaterThanEqual &);


    // PDTIfElse 
    virtual Traversal::RetType post(PDTIfElse &);


    // PDTImplies 
    virtual Traversal::RetType post(PDTImplies &);


    // PDTIntRange 
    virtual Traversal::RetType post(PDTIntRange &);


    // PDTInvariant 
    virtual Traversal::RetType post(PDTInvariant &);
    //virtual Traversal::RetType pre(PDTInvariant &);


    // PDTLessThan 
    virtual Traversal::RetType post(PDTLessThan &);


    // PDTLessThanEqual 
    virtual Traversal::RetType post(PDTLessThanEqual &);


    // PDTListOfStatements 
    virtual Traversal::RetType post(PDTListOfStatements &);


    // PDTMod 
    virtual Traversal::RetType post(PDTMod &);


    // PDTMult 
    virtual Traversal::RetType post(PDTMult &);


    // PDTNeg 
    virtual Traversal::RetType post(PDTNeg &);


    // PDTNilStatement 
    virtual Traversal::RetType post(PDTNilStatement &);


    // PDTNot 
    virtual Traversal::RetType post(PDTNot &);


    // PDTNotEqualBool 
    virtual Traversal::RetType post(PDTNotEqualBool &);


    // PDTNotEqualNum 
    virtual Traversal::RetType post(PDTNotEqualNum &);


    // PDTNumConst 
    virtual Traversal::RetType post(PDTNumConst &);


    // PDTNumConstDbl 
    virtual Traversal::RetType post(PDTNumConstDbl &);


    // PDTNumConstInt 
    virtual Traversal::RetType post(PDTNumConstInt &);


    // PDTNumVar 
    virtual Traversal::RetType post(PDTNumVar &);


    // PDTOr 
    virtual Traversal::RetType post(PDTOr &);


    // PDTPair 
    virtual Traversal::RetType post(PDTPair &);


    // PDTPostCondition 
    virtual Traversal::RetType post(PDTPostCondition &);
    virtual Traversal::RetType pre(PDTPostCondition &);


    // PDTPreCondition 
    virtual Traversal::RetType post(PDTPreCondition &);
    //virtual Traversal::RetType pre(PDTPreCondition &);


    // PDTProp 
    virtual Traversal::RetType post(PDTProp &);
    //virtual Traversal::RetType pre(PDTProp &);


    // PDTRelation 
    virtual Traversal::RetType post(PDTRelation &);


    // PDTSequence 
    virtual Traversal::RetType pre(PDTSequence &);


    // PDTSequenceAccessBool 
    virtual Traversal::RetType post(PDTSequenceAccessBool &);


    // PDTSequenceAccessNum 
    virtual Traversal::RetType post(PDTSequenceAccessNum &);


    // PDTSequenceAssign 
    virtual Traversal::RetType post(PDTSequenceAssign &);


    // PDTSequenceVar 
    virtual Traversal::RetType post(PDTSequenceVar &);


    // PDTSet 
    virtual Traversal::RetType post(PDTSet &);


    // PDTSetVar 
    virtual Traversal::RetType post(PDTSetVar &);

    // PDTSubt 
    virtual Traversal::RetType post(PDTSubt &);


    // PDTWhile 
    virtual Traversal::RetType post(PDTWhile &);


    // PDTXor 
    virtual Traversal::RetType post(PDTXor &);


    // PDTUnresolvedExp 
    virtual Traversal::RetType post(PDTUnresolvedExp &);


    // PDTType 
    virtual Traversal::RetType post(PDTType &);


    // PDTUnaryNumExpr 
    virtual Traversal::RetType post(PDTUnaryNumExpr &);

};
#endif
